Skip to content

Conversation

nilehmann
Copy link

@nilehmann nilehmann commented Aug 1, 2025

This PR adds flux specifications for checking the following modules in core

  • pat
  • bstr
  • hash
  • time

In particular, it verifies that Nanoseconds is correctly used with values within the range.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@nilehmann nilehmann requested a review from a team as a code owner August 1, 2025 00:51
Copy link
Member

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given I'm not intimately familiar with Flux some of the annotations introduced in this PR are not entirely clear to me, see detailed comments. Please include some comments. Thank you!

Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@carolynzech carolynzech enabled auto-merge August 13, 2025 17:44
@tautschnig tautschnig assigned nilehmann and unassigned carolynzech Aug 22, 2025
auto-merge was automatically disabled August 22, 2025 16:16

Head branch was pushed to by a user without write access

@nilehmann nilehmann removed their assignment Sep 9, 2025
@nilehmann
Copy link
Author

@tautschnig, sorry for the delay, but Flux is green again! After the toolchain update, we had to add a couple of extra specs included in 0375ccd

@tautschnig tautschnig enabled auto-merge September 9, 2025 19:45
@tautschnig tautschnig added this pull request to the merge queue Sep 9, 2025
Merged via the queue into model-checking:main with commit 398ff24 Sep 9, 2025
26 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants